YES 0.736 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/FiniteMap.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ CR

mainModule FiniteMap
  ((minFM :: FiniteMap () a  ->  Maybe ()) :: FiniteMap () a  ->  Maybe ())

module FiniteMap where
  import qualified Maybe
import qualified Prelude

  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a


  minFM :: Ord b => FiniteMap b a  ->  Maybe b
minFM EmptyFM Nothing
minFM (Branch key _ _ fm_l _) 
case minFM fm_l of
  Nothing-> Just key
  Just key1-> Just key1


module Maybe where
  import qualified FiniteMap
import qualified Prelude



Case Reductions:
The following Case expression
case minFM fm_l of
 Nothing → Just key
 Just key1 → Just key1

is transformed to
minFM0 key Nothing = Just key
minFM0 key (Just key1) = Just key1



↳ HASKELL
  ↳ CR
HASKELL
      ↳ BR

mainModule FiniteMap
  ((minFM :: FiniteMap () a  ->  Maybe ()) :: FiniteMap () a  ->  Maybe ())

module FiniteMap where
  import qualified Maybe
import qualified Prelude

  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a


  minFM :: Ord a => FiniteMap a b  ->  Maybe a
minFM EmptyFM Nothing
minFM (Branch key _ _ fm_l _) minFM0 key (minFM fm_l)

  
minFM0 key Nothing Just key
minFM0 key (Just key1Just key1


module Maybe where
  import qualified FiniteMap
import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
HASKELL
          ↳ COR

mainModule FiniteMap
  ((minFM :: FiniteMap () a  ->  Maybe ()) :: FiniteMap () a  ->  Maybe ())

module FiniteMap where
  import qualified Maybe
import qualified Prelude

  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a


  minFM :: Ord a => FiniteMap a b  ->  Maybe a
minFM EmptyFM Nothing
minFM (Branch key vw vx fm_l vyminFM0 key (minFM fm_l)

  
minFM0 key Nothing Just key
minFM0 key (Just key1Just key1


module Maybe where
  import qualified FiniteMap
import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
HASKELL
              ↳ Narrow

mainModule FiniteMap
  (minFM :: FiniteMap () a  ->  Maybe ())

module FiniteMap where
  import qualified Maybe
import qualified Prelude

  data FiniteMap a b = EmptyFM  | Branch a b Int (FiniteMap a b) (FiniteMap a b


  minFM :: Ord b => FiniteMap b a  ->  Maybe b
minFM EmptyFM Nothing
minFM (Branch key vw vx fm_l vyminFM0 key (minFM fm_l)

  
minFM0 key Nothing Just key
minFM0 key (Just key1Just key1


module Maybe where
  import qualified FiniteMap
import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
QDP
                  ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_minFM(Branch(wv30, wv31, wv32, wv33, wv34), h) → new_minFM(wv33, h)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: